(* $Id: parser.mly 117 2007-10-21 17:27:07Z yann.regisgianas $ *)

%{
  open CoreSyntax.Raw
  open CoreSyntaxRawExt
  open Position

  let parse_error = Error.error "during parsing"
%}

%token<string> ID BINOPLEFT1 BINOPLEFT2 BINOPRIGHT1 BINOPRIGHT2 BINOP0
%token<string> CONSTRUCTOR
%token VAL REC EQ TYPE MATCH WITH END DOT DEFERRED LEMMA AXIOM AND PREDICATE
%token INTTYPE BOOLTYPE UNITTYPE PROPTYPE EXISTS 
%token COLON COMMA LPAREN RPAREN DARROW LARROW ARROW LBRACK RBRACK STAR BAR
%token WHERE RETURNS FUN LET IN FORALL PRE POST INDUCTIVE LOGIC ABSURD
%token TRUEPROP FALSEPROP EOF TRUE FALSE IF THEN ELSE
%token OR IMPLY EQUIV NOT ASSERT LT GT GTE LTE PLUS MINUS SLASH
%token<int> INT

%nonassoc DOT IN
%right ARROW LARROW DARROW IMPLY EQUIV
%nonassoc ELSE
%left OR 
%left AND
%nonassoc EQ GTE GT LTE LT 
%left BINOPLEFT2 PLUS MINUS
%right BINOPRIGHT2 
%left BINOPLEFT1 STAR SLASH
%right BINOPRIGHT1 
%nonassoc BINOP0 
%nonassoc LPAREN 
%nonassoc LBRACK

%start<CoreSyntax.Raw.program> program

%%

(** A program is a list of components. *)

program: cs=located_components* e=located(empty) EOF
{
  let cs = List.flatten cs in
    List.fold_right 
      (fun c p -> PConsComponent (Position.position c, Position.value c, p)) cs
      (PEmpty (Position.position e))
}

(** Component. *)
located_components: cs=located(component)
{
  let pos = Position.position cs in
    List.map (Position.with_pos pos) (Position.value cs)
}

%public component:

(** Toplevel values *)

(** Deferred toplevel values. *)

  DEFERRED VAL lx=with_location(value_id) 
  f=optional_lformula COLON s=type_scheme 
{
  let (pos, x) = lx in
  let TScheme (ts, ty) = s in
    [ mk_value_component ts 
	([ (x, ([], ty)) ], f) (mk_lterm (pos, EDeferred)) ]
}

(** Deferred toplevel values. *)

| DEFERRED VAL lx=with_location(value_id) 
  f=optional_lformula COLON s=type_scheme WHERE p=lformula
{
  let (pos, x) = lx in
  let TScheme (ts, ty) = s in
    [ mk_value_component ts 
	([ (x, ([], ty)) ], f) (mk_lterm (pos, EDeferred));
      CFact (Axiom (UniqueIdentifier.fresh (p.fpos, "axiom")), p) ]
}

(** Toplevel basic values. *)

| LET ts=optional_type_parameters lt=logic_bindings EQ t=lterm
{
  [ mk_value_component ts lt t ]
}

(** Toplevel functional values. *)

| LET fdef=function_definition 
{
  let (ts, f, fdef) = fdef in
    [ mk_functional_component ts f fdef ]
}

(** Toplevel mutually recursive functions. *)

| LET REC fdef=function_definition 
  fdefs=list(preceded(AND, function_definition))
{
  [ mk_recursive_functions_component (fdef :: fdefs) ]
}

(** Type definition. *)

| TYPE x=type_id tdef=type_definition
{
  [ CTypeDef (x, fst tdef, snd tdef) ]
}

(** Deferred type definition. *)

| DEFERRED TYPE x=type_id COLON k=kind
{
  [ CTypeDef (x, k, DeferredType) ]
}

(** Lemma. *)

| LEMMA COLON f=lformula
{
  [ CFact (Lemma (UniqueIdentifier.fresh (f.fpos, "lemma")), f) ]
}

| LEMMA n=with_location(ID) COLON f=lformula
{
  [ CFact (Lemma (UniqueIdentifier.mk n), f) ]
}

(** Axiom. *)

| AXIOM COLON f=lformula
{
  [ CFact (Axiom (UniqueIdentifier.fresh (f.fpos, "axiom")), f) ]
}

| AXIOM n=with_location(ID) COLON f=lformula
{
  [ CFact (Axiom (UniqueIdentifier.mk n), f) ]
}

(** Predicate definitions. *)

(** Predicate abbreviation. *)

| PREDICATE x=predicate_id b=fbindings EQ f=lformula
{
  let d = mk_flexible_bounded_formula (fun b f -> FLam (b, f)) b f in
    [ CPredicate (x, PDAbbrev (mk_lformula (f.fpos, d))) ]
}

(** Deferred predicate. *)

| DEFERRED PREDICATE x=predicate_id COLON s=formula_type_scheme 
{
  let pos = PIdentifier.position x in 
  let FTScheme (ts, ty) = s in
  let d = 
    FForallTys (ts, 
		mk_lformula (pos, FAnnot (mk_lformula (pos, FDeferred), ty)))
  in
    [ CPredicate (x, PDAbbrev (mk_lformula (pos, d))) ]
}

(** Deferred predicate with axiomatization. *)

| DEFERRED PREDICATE x=predicate_id COLON s=formula_type_scheme 
  WHERE p=lformula
{
  let pos = PIdentifier.position x in 
  let FTScheme (ts, ty) = s in
  let d = 
    FForallTys (ts, 
		mk_lformula (pos, FAnnot (mk_lformula (pos, FDeferred), ty)))
  in
    [ CPredicate (x, PDAbbrev (mk_lformula (pos, d)));
      CFact (Axiom (UniqueIdentifier.fresh (p.fpos, "axiom")), p) ]
}

(** Logic function definition. *)

| LOGIC x=predicate_id fdef=logic_function_definition
{
  [ CLogicFunction (x, fdef) ]
}

(** Deferred logic function definition. *)

| DEFERRED LOGIC x=predicate_id COLON s=formula_type_scheme 
{
  let pos = PIdentifier.position x in 
  let FTScheme (ts, ty) = s in
  let d = 
    FForallTys (ts, 
		mk_lformula (pos, FAnnot (mk_lformula (pos, FDeferred), ty)))
  in
    [ CLogicFunction (x, LFAbbrev (mk_lformula (pos, d))) ]
}

(** Deferred logic function definition with axiomatization. *)

| DEFERRED LOGIC x=predicate_id COLON s=formula_type_scheme WHERE p=lformula
{
  let pos = PIdentifier.position x in 
  let FTScheme (ts, ty) = s in
  let d = 
    FForallTys (ts, 
		mk_lformula (pos, FAnnot (mk_lformula (pos, FDeferred), ty)))
  in
    [ CLogicFunction (x, LFAbbrev (mk_lformula (pos, d)));
      CFact (Axiom (UniqueIdentifier.fresh (p.fpos, "axiom")), p) ]
}

(** Inductive predicate definition. *)

| INDUCTIVE ts=optional_type_parameters x=predicate_id 
  ty=optional_formula_type
  EQ 
  b=optional_parameters 
  BAR is=separated_list(BAR, lformula)
{
  let ctx f = 
    let pos = f.fpos in
      mk_lformula 
	(pos, FForallTys 
	   (ts, 
	    mk_lformula (pos, mk_flexible_bounded_formula 
			   (fun b f -> FForall (b, [], f)) b f)))
  in
  let s = 
    match ty with
      | ([], ty) -> Some (FTScheme (ts, ty))
      | _ -> None
  in
    [ CPredicate (x, PDInductive (s, List.map ctx is)) ]
}

(** Syntax error. *)

| x=with_location (error)
{
  parse_error (fst x) "syntax error"
}


logic_clauses: BAR? lcs=separated_list(BAR, logic_clause)
{
  lcs
}

logic_clause: p=pattern ARROW f=lformula
{
  (p, f)
}

(** Logic function definition. *)
logic_function_definition:
  xs=logic_function_args EQ lcs=logic_clauses
{
  LFInductive (xs, lcs)
}

logic_function_args: LPAREN xs=separated_list(COMMA, value_id) RPAREN
{ 
  xs 
}
| x=value_id
{
  [ x ]
}

optional_parameters: empty
{
  []
}
| FORALL b=fbindings DOT
{
  b
}

(** Function definition using the syntax:

    (let|and) 
    [ts] f (x_1: tau_1, ..., x_n: tau_n) where F 
         returns (y_1: tau_1', ..., y_m: tau_m') where F = t *)

function_definition:
    ts=optional_type_parameters 
    f=value_id 
    largs=logic_arguments ins=logic_bindings outs=function_output EQ t=lterm
{
  (ts, f, (largs, ins, outs, t))
}

(** Term decorated with a location. *)

lterm: lt=with_location(term)
{
  mk_lterm lt
}

(** Term. *)

term: 

(** Variable *)

x=value_id
{
  EId x
}

(** Data constructor. *)

| x=constructor_id 
{
  EId x
}

(** Lambda abstraction. *)

| FUN a=logic_arguments l=logic_bindings o=function_output ARROW t=lterm
{
  mk_lam (a, l, o, t)
}

(** Application. *)

| f=lterm LPAREN args=separated_list(COMMA, lterm) RPAREN 
{
  match f.tvalue with

    | EId k when PIdentifier.is_constructor_id k ->
	EKApp (k, args)

    | _ ->
	EApp (f, [], args)
}

| f=lterm 
    LBRACK largs=separated_list(COMMA, lformula) RBRACK 
    LPAREN args=separated_list(COMMA, lterm) RPAREN 
{
  EApp (f, largs, args)
}

(** Binary operator application. *)

| l=lterm op=with_location(binop_value_id) r=lterm
{
  EApp (mk_lterm (fst op, EId (snd op)), [], [ l; r ])
}

(** Let binding. *)

| LET ts=optional_type_parameters l=logic_bindings EQ t1=lterm IN t2=lterm
{
  let (xs, f, t1) = mk_value ts l t1 in
    ELet (xs, f, t1, t2)
}

(** Let binding. *)

| LET REC fdef=function_definition IN t2=lterm
{
  let (ts, f, fdef) = fdef in
  let (xs, f, t1) = mk_functional_value ts f fdef in
    ELetRec (xs, f, t1, t2)
}

(** Irrefutable pattern. *)

| LET p=constructor_pattern EQ t1=lterm IN t2=lterm
{
  ECase (t1, [ (p, t2) ])
}

(** Case analysis. *)

| MATCH t=lterm WITH cs=clauses END
{
  ECase (t, cs)
}

(** Product. *)

| LPAREN args=separated_nonempty_list(COMMA, lterm) RPAREN
{
  EProd args
}

(** Primitive. *)

| p=primitive
{
  EPrimitive p
}

(** Conditional. *)

| IF c=lterm THEN t=lterm ELSE f=lterm
{
  EIf (c, t, f)
}

(** Dead code. *)

| ABSURD
{
  EAbsurd
}

(** Universal type quantification. *)

| FORALL ts=type_parameter+ DOT t=lterm
{
  EForallTys (ts, t)
}

(** Type annotation. *)

| LPAREN t=lterm COLON ty=term_type RPAREN
{
  EAnnot (t, ty)
}

(** Logic assertion. *)

| ASSERT f=lformula IN t=lterm
{
  EAssert (f, t)
}

(** Let-logic assertion. *)

| LET LOGIC bs=fbindings WHERE f=lformula IN t=lterm
{
  mk_flexible_bounded_term (fun b t -> ELetLogic (b, f, t)) bs t
}

(** Syntax error. *)

| x=with_location (error)
{
  parse_error (fst x) "syntax error."
}

(** Clauses of a case analysis. *)

clauses: BAR? cs=separated_list(BAR, clause) 
{
  cs
}

(** Clause. *)

clause: k=pattern ARROW t=lterm
{
  (k, t)
}

(** Pattern. *)

pattern: x=value_id
{
  PVar x
}
| cp=constructor_pattern
{
  cp
}

%inline constructor_pattern: k=constructor_id ts=type_parameters
{
  PApp (k, ts, [])
}
| k=constructor_id ts=type_parameters LPAREN ps=separated_list(COMMA, pattern) RPAREN
{
  PApp (k, ts, ps)
}

(** Primitive. *)

primitive: x=INT
{
  PInt x
}
| TRUE
{
  PTrue
}
| FALSE
{
  PFalse
}

(** Logic bindings. *)

logic_bindings: bs=bindings f=optional_lformula
{
  (bs, f)
}

logic_arguments: empty
{
  []
}
| LBRACK bs=separated_nonempty_list(COMMA, fbinding) RBRACK
{
  bs
}

bindings: LPAREN bs=separated_list(COMMA, binding) RPAREN
{
  bs
}
| x=value_id
{
  [ (x, wildcard ()) ]
}

binding: x=value_id COLON ty=term_type
{
  (x, ([], ty))
}
| x=value_id 
{
  (x, wildcard ())
}

(** Optional type parameters. *)

%inline optional_type_parameters: empty
{
  []
}
| LBRACK ts=type_parameters RBRACK
{
  ts
}

type_parameters: ts=type_parameter*
{
  ts
}

type_parameter: x=with_location(ID)
{
  PIdentifier.mk_type_id x
}

(** Function output. 

    If a function output is not given, one is 
    automatically generated. *)

function_output: p=with_location(empty) 
{
  mk_implicit_output (fst p)
}
| RETURNS l=logic_bindings
{
  l
}

(** Type scheme *)

type_scheme: ty=term_type 
{
  TScheme ([], ty)
}
| FORALL ts=type_parameters DOT ty=term_type
{
  TScheme (ts, ty)
}

(** Term type. *)

term_type: 

(** Primitive type. *)

  p=primitive_type
{
  TPrimitive p
}

(** Type variable. *)

| x=type_id
{
  TVar x
}

(** Type product. *)

| LPAREN tys=separated_nonempty_list(STAR, term_type) RPAREN
{
  TProd tys
}

(** Type application. *)

| x=type_id LPAREN args=separated_list(COMMA, term_type) RPAREN
{
  TApp (x, args)
}

(** Computational function type. *)

| ins=term_type ARROW outs=term_type
{
  TArrow (ins, outs)
}

primitive_type: 

(** Integers. *)

INTTYPE
{
  TInt
}

(** Booleans. *)

| BOOLTYPE
{
  TBool
}

(** Unit. *)

| UNITTYPE
{
  TUnit
}

(** Type definition. *)

type_definition:

(** Algebraic datatype definition. *)

ts=type_parameters EQ BAR? ds=separated_list(BAR, dataconstructor_def)
{
  (KArrow (Misc.repeat (List.length ts) (Misc.const KStar)), DAlgebraic (ts, ds))
}

(** Data constructor declaration. *)

dataconstructor_def:
k=constructor_id COLON ts=existential_parameters ty=term_type
{
  (k, ts, ty)
}

existential_parameters: empty
{
  []
}
| FORALL ts=type_parameters DOT
{
  ts
}

(** Kind. *)

kind: STAR
{
  KStar
}
| STAR ARROW STAR
{
  KArrow [KStar]
}
| LPAREN ks=separated_nonempty_list(COMMA, kind) RPAREN ARROW STAR
{
  KArrow ks
}

(** Optional formula decorated with a location. *)

optional_lformula: p=with_location(empty) 
{
  ImplicitFormula (fst p)
}
| WHERE f=where_lformula
{
  ExplicitFormula f
}

(** Formula decorated with a location. *)

lformula: lf=with_location(formula) 
{
  mk_lformula lf
}

(** Formula. *)

formula: 

(** True proposition. *)

TRUEPROP
{
  FTrue
}

(** False proposition. *)

| FALSEPROP
{
  FFalse
}

(** Logical value. *)

| x=value_id
{
  FVar x
}
| x=constructor_id 
{
  FVar x
}

| p=primitive
{
  FPrimitive (PEPrimitive p)
}

(** Universal quantification. *)

| FORALL b=fbindings tgs=triggers DOT f=lformula
{
  mk_flexible_bounded_formula (fun b f -> FForall (b, tgs, f)) b f
}

(** Existential quantification. *)

| EXISTS b=fbindings DOT f=lformula
{
  mk_flexible_bounded_formula (fun b f -> FExists (b, f)) b f
}

(** Logical lambda abstraction. *)

| FUN b=fbindings DARROW f=lformula
{
  mk_flexible_bounded_formula (fun b f -> FLam (b, f)) b f
}

(** Application. *)

| f=lformula
  LPAREN args=separated_list(COMMA, lformula) RPAREN 
{
  match f.fvalue with

    | FVar k when PIdentifier.is_constructor_id k ->
	FKApp (k, args)

    | _ ->
	FApp (f, args)
}

| PRE LPAREN f=value_id RPAREN 
  LPAREN args=separated_list(COMMA, lformula) RPAREN 
{
  let pos = PIdentifier.position f in
    mk_fapp pos 
      (mk_fapp pos 
	 (mk_fapp pos (FPrimitive Pre) [ mk_lformula (pos, FVar f) ]) 
	 [])
      args
}

| POST LPAREN f=value_id RPAREN 
  LPAREN args1=separated_list(COMMA, lformula) RPAREN 
  LPAREN args2=separated_list(COMMA, lformula) RPAREN 
{
  let pos = PIdentifier.position f in
    mk_fapp pos
      (mk_fapp pos 
	 (mk_fapp pos 
	    (mk_fapp pos (FPrimitive Post) [ mk_lformula (pos, FVar f) ]) 
	    [])
	 args1)
      args2
}

(** Product. *)

| LPAREN args=separated_nonempty_list(COMMA, lformula) RPAREN
{
  match args with
    | [ f ] -> f.fvalue
    | args -> FProd args
}

(** Logical primitive. *)

| p=formula_primitive 
{
  FPrimitive p
}

| p=binary_formula_primitive 
{
  FPrimitive p
}

(** Binary operation. *)

| l=lformula f=with_location(binpid_or_formula_primitive) r=lformula
{
  FApp (mk_lformula f, [ l; r ])
}

(** Equality between values. *)

| v1=lformula EQ v2=lformula 
{
  FEq (v1, v2)
}


(** Formula without toplevel equality. *)

where_formula: 

(** True proposition. *)

TRUEPROP
{
  FTrue
}

(** False proposition. *)

| FALSEPROP
{
  FFalse
}

(** Predicate. *)

| p=predicate_id
{
  FVar p
}

(** Logical value. *)

(** Subset of formulae that describes values. *)

| x=constructor_id 
{
  FVar x
}

| p=primitive
{
  FPrimitive (PEPrimitive p)
}

(** Polymorphic formula. *)

| FORALL LBRACK ts=type_parameter+ RBRACK DOT f=lformula
{
  FForallTys (ts, f)
}

(** Introduction of flexible type variables. *)

| EXISTS LBRACK ts=type_parameter+ RBRACK DOT f=lformula
{
  FExistsTys (ts, f)
}

(** Universal quantification. *)

| FORALL b=fbindings tgs=triggers DOT f=lformula
{
  mk_flexible_bounded_formula (fun b f -> FForall (b, tgs, f)) b f
}

(** Existential quantification. *)

| EXISTS b=fbindings DOT f=lformula
{
  mk_flexible_bounded_formula (fun b f -> FExists (b, f)) b f
}

(** Logical lambda abstraction. *)

| FUN b=fbindings DARROW f=lformula
{
  mk_flexible_bounded_formula (fun b f -> FLam (b, f)) b f
}

(** Application. *)
| f=where_lformula
  LPAREN args=separated_list(COMMA, lformula) RPAREN 
{
  match f.fvalue with

    | FVar k when PIdentifier.is_constructor_id k ->
	FKApp (k, args)

    | _ ->
	FApp (f, args)
}

| PRE LPAREN f=value_id RPAREN 
  LPAREN args=separated_list(COMMA, lformula) RPAREN 
{
  let pos = PIdentifier.position f in
    mk_fapp pos 
      (mk_fapp pos 
	 (mk_fapp pos (FPrimitive Pre) [ mk_lformula (pos, FVar f) ]) 
	 [])
      args
}

| POST LPAREN f=value_id RPAREN 
  LPAREN args1=separated_list(COMMA, lformula) RPAREN 
  LPAREN args2=separated_list(COMMA, lformula) RPAREN 
{
  let pos = PIdentifier.position f in
    mk_fapp pos
      (mk_fapp pos 
	 (mk_fapp pos 
	    (mk_fapp pos (FPrimitive Post) [ mk_lformula (pos, FVar f) ]) 
	    [])
	 args1)
      args2
}

(** Grouping. *)

| LPAREN f=formula RPAREN
{
  f
}

(** Logical primitive. *)

| p=formula_primitive 
{
  FPrimitive p
}

| p=binary_formula_primitive 
{
  FPrimitive p
}

(** Binary operation. *)

| l=where_lformula f=with_location(binpid_or_formula_primitive) r=lformula
{
  FApp (mk_lformula f, [ l; r ])
}

where_lformula: f=with_location(where_formula)
{
  mk_lformula f
}

(** Logical primitives. *)

formula_primitive: 
NOT
{
  PNot
}

%inline binary_formula_primitive: 
  AND
{
  PAnd
}
| OR
{
  POr
}
| IMPLY
{
  PImply 
}
| EQUIV
{
  PEquiv
}
| LT
{
  PLessThan
}
| GT
{
  PGreaterThan
}
| LTE
{
  PLessEqualThan
}
| GTE
{
  PGreaterEqualThan
}
| PLUS
{
  PAdd
}
| MINUS
{
  PSub
}
| STAR
{
  PMult
}
| SLASH
{
  PDiv
}


%inline binpid_or_formula_primitive:
p=binary_formula_primitive
{
  FPrimitive p
}
| x=binop_predicate_id
{
  FVar x
}

(** Logical bindings. *)

fbindings: LPAREN bs=separated_list(COMMA, fbinding) RPAREN
{
  bs
}
| x=value_id s=optional_formula_type
{
  [ (x, s) ]
}

fbinding: x=value_id s=optional_formula_type
{
  (x, s)
}

triggers: empty
{
  []
}
| LBRACK tgs=separated_list(COMMA, value_id) RBRACK
{
  tgs
}

(** Optional formula type. *)

optional_formula_type: empty
{
  fwildcard ()
}
| COLON fty=formula_type
{
  ([], fty)
}

formula_type: 

(** Type of proposition. *)

 PROPTYPE
{
  FTProp
}

(** Logical type variable. *)

| x=type_id
{
  FTVar x
}

(** Logical function type. *)

| ty1=formula_type LARROW ty2=formula_type
{
  FTArrow (ty1, ty2)
}

(** Computational function type. *)

| ty1=formula_type ARROW ty2=formula_type
{
  FTCArrow (ty1, ty2)
}

(** Primitive type. *)

| p=primitive_type
{
  FTPrimitive p
}

(** Product type. *)

| LPAREN tys=separated_nonempty_list(STAR, formula_type) RPAREN
{
  FTProd tys
}


(** Formula type scheme *)

formula_type_scheme: ty=formula_type 
{
  FTScheme ([], ty)
}
| FORALL ts=type_parameters DOT ty=formula_type
{
  FTScheme (ts, ty)
}

(** Identifiers. *)

%inline value_id: x=with_location(ID)
{
  PIdentifier.mk_value_id x
}
| x=with_location(binop) 
{
  PIdentifier.mk_value_id x
}

%inline binop_value_id: x=with_location(binop)
{
  PIdentifier.mk_value_id x
}

%inline constructor_id: x=with_location(CONSTRUCTOR)
{
  PIdentifier.mk_value_id ~is_constructor:true x
}

%inline type_id: x=with_location(ID)
{
  PIdentifier.mk_type_id x
}

%inline predicate_id: x=with_location(ID)
{
  PIdentifier.mk_value_id x
}
| x=with_location(binop) 
{
  PIdentifier.mk_value_id x
}

%inline binop_predicate_id: x=with_location(binop)
{
  PIdentifier.mk_value_id x
}

%inline binop: 
x=BINOPLEFT1 | x=BINOPLEFT2 | x=BINOPRIGHT1 | x=BINOPRIGHT2 | x=BINOP0
{
  x
}

(** Misc. *)

%public %inline located(x) : x=x
{
  Position.with_pos (Position.lex_join $startpos $endpos) x
}

%public %inline with_location(x) : x=x
{
  (Position.lex_join $startpos $endpos, x)
}

%public %inline with_location2(x) : x=x
{
  (Position.lex_join $startpos $endpos, fst x, snd x)
}

%inline empty: /* empty */ { () }
